; <lemma>
;  <title>ch912_mobile.1</title>
;  <origin>ch912_mobile | mobile_2 | thm1/THM</origin>
(benchmark ch912_mobile_1
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="X" type="POW(INTEGER)"/>
  :extrapreds ((X Int))
;    <variable name="k" type="INTEGER"/>
;  </typenv>
  :extrafuns ((k Int))
;  m <-> max(X)
  :extrafuns ((m Int))
  :extramacros (
		 (Nat (lambda (?i Int) . (<= 0 ?i)))
		 (emptyset (lambda (?x 't). false))
		 (in (lambda (?x 't) (?p ('t boolean)) . (?p ?x)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 (subseteq
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (forall (?x 't). 
		       (implies (?p ?x) (?q ?x)))))
		 (range1 (range 0 k))
		 (ismax
		   (lambda (?m Int) (?pi (Int boolean))  .
		     (and (?pi ?m)
		       (forall (?i1 Int) . (implies (?pi ?i1) (<= ?i1 ?m))))))
		 )
; <hypothesis needed="true">k : NATURAL</hypothesis>
  :assumption (in k Nat)
; <hypothesis needed="true">X <: 0 .. k</hypothesis>
  :assumption (subseteq X range1)
; <hypothesis needed="true">not X = {}</hypothesis>
  :assumption (not (= X emptyset))
; m <-> max(X)
  :assumption (ismax m X)
; <goal>max(X) <= k</goal>
  :formula
  (not
      (<= m k)
    )
)
; </lemma>

